:- module(fd_sbds). :- export sbds_initialise_body / 6. :- export sbds_initialise_body / 5. :- export unify_sbds / 2. :- export print_sbds / 2. :- export sbds_get_matrix / 2. :- export sbds_get_index / 2. :- export is_sbds_var / 1. :- export sbds_try / 2. :- export sbds_initialise / 5. :- export sbds_initialise / 4. :- comment(summary, "Symmetry Breaking During Search (SBDS)"). :- comment(desc, "Symmetry Breaking During Search (SBDS) library, provides predicates to initalise symmetry breaking during search search and to perform the search, as well as utility functions for prining and unification."). :- comment(author, "Warwick Harvey & Karen Petrie"). :- comment(date, "$Date: 2002/11/19 21:47:57 $"). :- comment(is_sbds_var / 1, [summary : "checks whether a variable is an SBDS variable", args : ["Var" : "Variable to check"], amode : is_sbds_var(?), see_also : [sbds_initialise / 4, sbds_initialise / 5], desc : html("\tSucceeds if and only if Var is a variable and has been initialised\n\tas an SBDS variable (through a call to sbds_initialise/4 or\n\tsbds_initialise/5)."), fail_if : "Var is not a variable or not an SBDS variable."]). :- comment(sbds_get_index / 2, [summary : "get the index of an SBDS attributed variable", args : ["Var" : "SBDS variable", "Idx" : "The index of Var"], amode : sbds_get_index(?, -), desc : html("\tUnifies Idx with the index of the SBDS variable Var. The index of\n\tthe variable is its position in the matrix provided in the\n\tcorresponding call to sbds_initialise/4 or sbds_initialise/5"), fail_if : "Var is not an SBDS variable."]). :- comment(sbds_get_matrix / 2, [summary : "get the matrix (array) of SBDS attributed variables", args : ["Var" : "SBDS variable", "Matrix" : "The matrix that Var appears in"], amode : sbds_get_matrix(?, -), desc : html("\tUnifies Matrix with the matrix (array) provided to a call to\n\tsbds_initialise/4 or sbds_initialise/5 which contains Var."), fail_if : "Var is not an SBDS variable."]). :- comment(sbds_initialise / 4, [summary : "Initialises the data needed for sbds", args : ["VarMatrix" : "Matrix of Search Variables", "SymPreds" : "List of symmetry predicates", "FixPred" : "Predicate to assign a variable to a value", "Options" : "List of Options to use during search"], amode : sbds_initialise(+, +, ++, +), see_also : [sbds_initialise / 5, sbds_try / 2], desc : html("

Symmetry Predicates

\n\tVarMatrix, is the matrix of variables, which are searched over to allocate \t\tvalues to, in this case a 1-dimensonal matrix, for the n-dimensonal case see \t\tsbds_initalise/5.\n\t
\n\t
\n\tThe symmetry predicates should transform a variable and value to there \n\tsymmetrical equivalent. The last four arguments of these predicates should \n\ttherefore be the original variable, the original value (which are input) then \t\tthe symmetrical variable and the symmetrical value (which are output). Before \t\tthese parameters you can give any other parameters which are useful in your \t\timplementation\n\ti.e. the matrix of variables. So my symmetry predicate might be:\n\tsymmetry_predicate(Matrix, Var, Val, SymVar, SymVal).\n\t
\n\t
\n\tWhen creating the list of symmetry predicates (the parameter given to \t\t\tsbds_initalise), \n\tyou only need to specify the parameters that you have added. So for the above \t\tpredicate,\n\tthe entry to the list would be: symmetry_predicate(Matrix)\n\tThis is shown below in the N-Queens model.\n\t
\n\t
\n\tThe FixPred is the predicate which will fix and exclude a variable to a value \t\tat decision points in the search tree, it must have three parameters the first \t\ttwo will be the variable and the value, and the third will be a boolean which \t\tspecifies whether the variable is being fixed or excluded i.e. is this \t\t\tconstraint true or false. #= / 3, is usually used for thse purposes.\n\t
\n\t
\n\tThe Options list, will be a list of options which can be used during search \t\ti.e. whether SBDS should be used at every node of the search tree. None of \t\tthese options are implemented as yet, so it should always be an empty list.\n\t

What SBDS initialise does:

\n\tCalled before search commences. Sets up the symmetries to indicate that \t\t\n\tthey are all unbroken initally and initalises all the variables etc. that will \t\tbe utilised during search."), exceptions : [abort : "Options is not an empty list"], eg : html("

Nqueens using a 1 dimensonal array

\n\t

The Symmetry Predicates for Nqueens Symmetries:

\n\t

r90(Matrix, N, Index, Value, SymVar, SymValue) :-: SymVar is Matrix[Value],; SymValue is N + 1 - Index.

\n\t\n\t

r180(Matrix, N, Index, Value, SymVar, SymValue) :-: SymVar is Matrix[N + 1 - Index],; SymValue is N + 1 - Value.

\n\t\n\t

r270(Matrix, N, Index, Value, SymVar, SymValue) :-: SymVar is Matrix[N + 1 - Value],; SymValue is Index.

\n\n\t

rx(Matrix, N, Index, Value, SymVar, SymValue) :-: SymVar is Matrix[N + 1 - Index],; SymValue is Value.

\n\n\t

ry(Matrix, N, Index, Value, SymVar, SymValue) :-: SymVar is Matrix[Index],; SymValue is N + 1 - Value.

\n\n\t

rd1(Matrix, _N, Index, Value, SymVar, SymValue) :-: SymVar is Matrix[Value],; SymValue is Index.

\n\n\t

rd2(Matrix, N, Index, Value, SymVar, SymValue) :-: SymVar is Matrix[N + 1 - Value],; SymValue is N + 1 - Index.

\n\t\t\n\t

Then to initialise SBDS

\n\t

Matrix =.. [[] | Board],
%The list of symmetry predicates,
Syms = [: r90(Matrix, N),; r180(Matrix, N),; r270(Matrix, N),; rx(Matrix, N),; ry(Matrix, N),; rd1(Matrix, N),; rd2(Matrix, N)
],
%the call to sbds_initalise,
sbds_initialise(Matrix, Syms, #=, []).

")]). :- comment(sbds_initialise / 5, [summary : "Initialises the data needed for sbds", args : ["VarMatrix" : "Matrix of Search Variables", "NDims" : "The Dimenson of VarMatrix", "SymPreds" : "List of symmetry predicates", "FixPred" : "Predicate to assign a variable to a value", "Options" : "List of Options to use during search"], amode : sbds_initialise(+, ++, +, ++, +), see_also : [sbds_initialise / 4, sbds_try / 2], desc : html("

Symmetry Predicates

\n\tVarMatrix, is the matrix of variables, which are searched over to allocate \t\tvalues to.\n\t
\n\t
\n\tNDims is the dimenson of VarMatrix\n\t
\n\t
\n\tThe symmetry predicates should transform a variable and value to there \n\tsymmetrical equivalent. The last four arguments of these predicates should \n\ttherefore be the original variable, the original value (which are input) then \t\tthe symmetrical variable and the symmetrical value (which are output). Before \t\tthese parameters you can give any other parameters which are useful in your \t\timplementation i.e. the matrix of variables. So my symmetry predicate might be:\n\tsymmetry_predicate(Matrix, Var, Val, SymVar, SymVal).\n\t
\n\t
\n\tWhen creating the list of symmetry predicates (the parameter given to \t\t\tsbds_initalise), you only need to specify the parameters that you have added. \t\tSo for the above predicate, the entry to the list would \t\t\t\tbe: symmetry_predicate(Matrix).\n\tThis is shown below in the N-Queens model.\n\t
\n\t
\n\tThe FixPred is the predicate which will fix and exclude a variable to a value \t\tat decision points in the search tree, it must have three parameters the first \t\ttwo will be the variable and the value, and the third will be a boolean which \t\tspecifies whether the variable is being fixed or excluded i.e. is this \t\t\tconstraint true or false. #= / 3, is usually used for thse purposes.\n\t
\n\t
\n\tThe Options list, will be a list of options which can be used during search \t\ti.e. whether SBDS should be used at every node of the search tree. None of \t\tthese options are implemented as yet, so it should always be an empty list.\n\t

What SBDS initialise does:

Nqueens using a boolean encoding on a 2 dimensonal array

\n\t

The Symmetry Predicates for Nqueens Symmetries:

\n\t

r90(Matrix, N, [X,Y], Value, SymVar, SymValue) :-: SymX is Y,; SymY is (N + 1 - X),; SymVar is Matrix[SymX, SymY],; SymValue is Value.

\n\t

r180(Matrix, N, [X,Y], Value, SymVar, SymValue) :-: SymX is (N + 1 - X),; SymY is (N + 1 - Y),; SymVar is Matrix[SymX, SymY],; SymValue is Value.

\n\t

r270(Matrix, N, [X,Y], Value, SymVar, SymValue) :-: SymX is (N + 1 - Y),; SymY is X,; SymVar is Matrix[SymX, SymY],; SymValue is Value.

\t\n\t

rx(Matrix, N, [X,Y], Value, SymVar, SymValue) :-: SymX is (N + 1 - X),; SymY is Y,; SymVar is Matrix[SymX, SymY],; SymValue is Value.

\n\t

ry(Matrix, N, [X,Y], Value, SymVar, SymValue) :-: SymX is X,; SymY is (N + 1 - Y),; SymVar is Matrix[SymX, SymY],; SymValue is Value.

\n\t

rd1(Matrix, _N, [X,Y], Value, SymVar, SymValue) :-: SymX is Y,; SymY is x,; SymVar is Matrix[SymX, SymY],; SymValue is Value.

\n\t

rd2(Matrix, N, [X,Y], Value, SymVar, SymValue) :-: SymX is (N + 1 - Y),; SymY is (N + 1 - X),; SymVar is Matrix[SymX, SymY],; SymValue is Value.

\n\t

Then to initialise SBDS

\n\t

%The list of symmetry predicates,

\n\t

Syms = [

\n\t\t

r90(Matrix, N),

\n\t\t

r180(Matrix, N),

\n\t\t

r270(Matrix, N),

\n\t\t

x(Matrix, N),

\n\t\t

y(Matrix, N),

\n\t\t

d1(Matrix, N),

\n\t\t

d2(Matrix, N)

\n\t

%the call to sbds_initalise,

\n\t

sbds_initialise(Matrix, 2, Syms, #=, []).

")]). :- comment(sbds_try / 2, [summary : "tries to assign a variable to a value", args : ["Var" : "SBDS Variable", "Val" : "Value to try and assign to Value"], amode : sbds_try(?, ++), see_also : [sbds_initialise / 4, sbds_initialise / 5], desc : html("Called for each variable, value pair tried at a decision point \t\tduring search.\n\t
\n\t
\n\tInitally tries to assign a variable to a value, if this is succesful then it \t\tupdates the symmetry functions to take account of any symmetries which have \t\tbeen broken by this assignment.\n\t
\n\t
\n\tIf this assignment is unsuccesful then it stipulates that the variable cannot \t\tbe assigned to this value, before placing constraints to eliminate the \t\t\tsymmetrical equivalent of this assgnment. If these symmetries are not already \t\tbroken"), exceptions : [abort : "Var is not an sbds attributed variable"], eg : html("

Replacement for labeling/1 which takes SBDS into account \t\t

\n\t

sbds_labeling(AllVars) :-: ( foreach(Var, AllVars) do; ).

\n\t

Replacement for indomain/1 which takes SBDS into account.

\n\t

% value ordering is input order
sbds_indomain(X) :-: nonvar(X).
sbds_indomain(X) :-: var(X),; mindomain(X, LWB),; %sbds_try called here; sbds_try(X, LWB),; sbds_indomain(X).

")]). :- comment(sbds_initialise_body / 6, hidden). :- comment(sbds_initialise_body / 5, hidden).